COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\section{Some simple examples of proofs}
C00022 00003	The next proposition is a fundamental relation between append and reverse.
C00027 ENDMK
C⊗;
\section{Some simple examples of proofs}
\sectlab{simple}

In this section we shall prove some simple properties of some simple 
programs. Our first example deals with the program /append/. As promised
in \sectref{adding funs} we begin by proving:

\noindent{\bf Proposition:} $\forall X\ [X\qapp y \not=\bot \liff X\in \qL!]$

We restate the definition of /append/ here for the readers convenience.
$$x\qapp y \leftarrow \qif \qn x \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$

\noindent{\bf Proof:} By the bottom axiom for the function \qapp\ we know that
$\bot\qapp y=\bot$, and as $\bot\not\in\qS!$ we know that $\bot\not\in\qL!$.
What remains for us to prove is that 
$$\forall x\ [x\qapp\ y \not= \bot \liff x\in\qL!]$$
which we prove by induction on the rank of $x$, our rank function being
$r↓{sexp}$ and $\Phi[x]$ being
$$x\qapp\ y \not= \bot \liff x\in\qL!.$$

To prove $\forall x\Phi[x]$,which is our aim, we need only prove
$$\forall x[\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]].$$
 In other words we must prove, for each $x\in\qS!$  that the assumption
$$\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]$$
(often called the /induction/ /hypothesis/) implies
$$\Phi[x].$$
It is at this point that we split the proof into two cases. The first case
corresponds to when $x$ is of least rank, in which case the induction hypothesis
is trivially true and so not of much use. The second case then is when $x$ is
not of least rank. Since we are using the rank function $r↓{sexp}$ these cases
correspond to when $x\in\qA!$ and when $x\in\qC!$.

\noindent{\bf Base case:} $r↓{sexp}(x)=0$, or in clearer terms $x\in\qA!$. By the 
program axiom for append we have
$$x\qapp y = \qif \qn x \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$
and we also have the two possibilities, either $x=|NIL|$ or $x\not=\qNIL$.

In the former case
$$x\qapp y = \qif \qT \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$
by the null axiom, and now by the if axiom we have
$$x\qapp y = y$$

In the later case we have 
$$x\qapp y = \qif \qNIL \qthen y \qelse \qa x \qcons [\qd x \qapp y]$$
by the null axiom, so by the if axiom we have
$$x\qapp y = \qa x \qcons [\qd x \qapp y]$$
but by the car axiom we know $\qa x = \bot$ so this becomes
$$x\qapp y = \bot \qcons [\qd x \qapp y]$$
and consequently by the cons axiom
$$x\qapp y = \bot$$

Thus we have proved that when $x$  is an atom then
$$x=\qNIL \supset x\qapp y\not= \bot$$
$$x\not=\qNIL \supset x\qapp y= \bot$$

Now since
$\qL! = \{|NIL|\} \cup [ \qS! \times \qL!]$ and
$\qS!\times\qL! \subset \qC!$ by the mapping equations, the above is simply
$$x\qapp\ y \not= \bot \liff x\in\qL!.$$
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} Suppose $x\in\qC!$ and assume the induction hypothesis,
namely,
$$\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]$$

Firstly observe that by the definition of \qL! we have, in this case,
$$x\in\qL! \liff \qd x\in\qL!$$
Now since $r↓{sexp}(\qd x)<r↓{sexp}(x)$ we can use the induction hypothesis
to conclude 
$$\qd x\qapp\ y \not= \bot \liff \qd x\in\qL!.$$

Finally since $x\in\qC!$ we have that $\qa x \not=\bot$ and so by the cons axiom 
we know that
$$\qa x\qcons[\qd x \qapp y]= \bot \liff  \qd x \qapp y = \bot$$
and using the program axiom we have 
$$x\qapp y = \qa x \qcons [\qd x \qapp y]$$
and putting all these equivalences together gives us the desired conclusion
$$x\qapp\ y \not= \bot \liff x\in\qL!.$$
$\qed↓{\bf induction\ step}$

Putting the base case and the induction step together shows that for every
$x\in\qS!$
$$\forall x[\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]].$$
and so by the rank induction principle we conclude
$$\forall x \Phi[x]$$
$\qed↓{\bf proposition}$
We shall now prove some algebraic properties of /append/. Not surprisingly
most of the nice properties of /append/ are only true when the function
is restricted to \qL!. In fact a simple elaboration of the last proof will show
that \qapp\ is an operation on \qL!:

\exercise $\qapp\ : \qL!\times\qL! \to\qL!$

Our first simple property expresses the fact that  |NIL| is both the left and
the right identity of the operation \qapp\ .

\noindent{\bf Proposition:} $|NIL|\qapp u = u\qapp|NIL| = u$

\noindent{\bf Proof:} The fact that $|NIL|\qapp u = u$ follows simply from the 
program, null and if axioms, since

$|NIL|\qapp u$

$= \qif \qn |NIL| \qthen u \qelse \qa |NIL| \qcons [\qd |NIL| \qapp u]$

$= \qif \qT \qthen u \qelse \qa |NIL| \qcons [\qd |NIL| \qapp u]$

$= u$

In future we shall not write out these simple reductions in such detail since
they become quite tedious, time consuming and they detract from the
essential points in the argument.

Now we prove the second part of the proposition, that
$$u\qapp |NIL| = u$$
We prove this by the /relativised/ /rank/ /induction/ /schema/ 

\noindent{\bf Rank Induction:}  $\forall u[\forall v[[r(v)<r(u)]\supset \Phi[v]] \supset
\Phi[u]] \supset \forall u \Phi[u]$

\exercise Prove that the relativized rank induction shema follows from the usual one.

 We prove by induction
on the rank of u, where the rank function is $r↓{list}$, that
$\forall u \Phi[u]$ where $\Phi[u]$ is simply
$$u\qapp |NIL| = u.$$

\noindent{\bf Base case:} In this case $r↓{list}(u)=0$ so $u=|NIL|$ and $\Phi[|NIL|]$
follows from the previous case.
$\qed↓{\bf base\ case}$

\noindent{\bf Induction step:} Suppose that $r↓{list}(u)>0$ ( i.e $u\in\qL{non-empty}$)
and that $\Phi [v]$ is true 
for all lists of less rank than $u$. In other words
$$\forall u[\forall v[[r(v)<r(u)]\supset \Phi[v]] \supset \Phi[u]]$$
then
$$u\qapp |NIL| = \qa u \qcons[ \qd u \qapp |NIL|]$$
by the if and null axioms.
But by the induction hypothesis $\qd u \qapp |NIL| = \qd u$ so we have
$$u\qapp |NIL| = \qa u \qcons  \qd u $$
and this is just $u$ by the cons axiom.
$\qed↓{\bf induction\ step}$

So we have shown that $\Phi[|NIL|]$ is true and that assuming the induction
hypothesis $\Phi[u]$ is true for all $u\in\qL{non-empty}$ thus we may conclude
$$\forall u \Phi[u]$$
$\qed↓{\bf proposition}$
We now prove that the append operation is associative. Thus showing that
the set \qL! together with the operation \qapp\ forms  what mathematicians call
a semigroup with identity.

\noindent{\bf Proposition:}
$\forall u,v,w\ u\qapp[v\qapp w] = [u\qapp v]\qapp w$

\noindent{\bf Proof:} Pick any $v,w\in \qL!$, we will show by induction on $r↓{list}(u)$ that
$$\forall u\ u\qapp[v\qapp w] = [u\qapp v]\qapp w$$
with $\Phi[u]$ being
$$u\qapp[v\qapp w] = [u\qapp v]\qapp w$$

\noindent{\bf Base  case:} $r↓{list}(u)=0$,i.e $u =|NIL|$ . This case is trivial since
$$u\qapp [v\qapp w] =
|NIL|\qapp[v \qapp w] =
[v \qapp w] =
[|NIL|\qapp v] \qapp w $$
by the previous proposition. $\qed↓{base\ case}$

\noindent{\bf Induction step:} In this case $u \in \qL{non-empty}$ and
assume that $\Phi[u↓0]$ holds for all lists $u↓0$ less than $u$. Then
$$u\qapp[v\qapp w] = \qa u \qcons [\qd u \qapp [v\qapp w]]$$
and by the induction hyputhesis
$$\qd u\ \qapp[v\qapp w] = [\qd u\qapp v]\qapp w]$$
so we have
$$u\qapp[v\qapp w] = \qa u \qcons[[\qd u \qapp  v]\qapp w]$$
Now we need the lemma

\noindent{\bf Lemma:} 
$\forall x,u,v\  x \qcons [u \qapp v] = [x \qcons u]\qapp v$

Leaving aside the proof of the lemma for a moment, we can use it immediately to 
obtain
$$u\qapp[v\qapp w] = [\qa u \qcons [\qd u \qapp  v]]\qapp w $$
and again to get
$$u\qapp[v\qapp w] =[[\qa u \qcons  \qd u] \qapp  v]\qapp w $$
but this is just
$$u\qapp[v\qapp w] =[u \qapp  v]\qapp w $$
$\qed↓{\bf induction\ step}$

We finish of the proof of the proposition by proving the lemma.

\noindent{\bf Proof of lemma:} Pick any $x,u,v$ then
$$[x \qcons u]\qapp v= \qa [ x\qcons u] \qcons [\qd[x\qcons u]\qapp v]$$
which reduces to
$$[x \qcons u]\qapp v=  x \qcons [ u\qapp v]$$
$\qed↓{\bf lemma\ and\ theorem}$

  The algebra of this proof is rather typical. 
We used the definition of the function involved several times, 
we used the induction hypothesis once, 
and we used the elementary algebraic facts about conditional
expressions and the basic functions of \lisp.
Also in this proof it does not matter whether we take $\Phi[u]$ to be
$u*[v\qapp w]=[u\qapp v]\qapp w$ or
$\forall v,w\ u*[v\qapp w]=[u\qapp v]\qapp w$   .
 The difference being that
in the first case the induction hypothesis is only refers to the particular
$v$ and $w$ of the conclusion while in the second case it applies to any
lists $v$, $w$.  When proving properties of recursively defined functions,
the unquantified form of $\Phi$ is generally good enough when the 
function definion does not modify the parameters (non-recursion arguments) in
recursive calls.  If it passes functions of the parameters in recursive
calls then it may be necessary to use the quantified version of $\Phi$.
In the next lemma we will need a quantified version.

The next few examples deal with the behavior of /reverse/, /reverse1/ and
/append/.
Recall that /reverse1/ and /reverse/ were defined by the programs.

$$/reverse1/[x] \leftarrow \qif \qn x \qthen |NIL| \qelse reverse1[\qd x]\qapp <\qa x>$$
$$/reverse/[x] \leftarrow /rev/[x,|NIL|]$$
$$rev[x,y]\leftarrow \qif \qn x \qthen y \qelse rev[\qd x, \qa x\qcons y]$$

We restrict our attention to the behaviour of these functions on \qL! because
of the following straightforward after reading the proof of the main lemma
below.
\exercise Show that $\forall x [/reverse/[x]\not=\bot\liff x\in\qL!]$
\exercise Show that $\forall x [/rev/[x,y]\not=\bot\liff x\in\qL!]$
\exercise Show that $\forall x [/reverse1/[x]\not=\bot\liff x\in\qL!]$

We said in \chapref{readin} that the functions /reverse/ and /reverse1/ were the
same. Our first task will be be to prove this fact

\noindent{\bf Proposition:} $\forall u\  /reverse/[u] = /reverse1/[u]$

Before we begin the proof of  this proposition we must prove a property concerning
/rev/. Notice that the previous exercises imply that we actually have
$\forall X\  /reverse/[X] = /reverse1/[X]$.

\noindent{\bf Main Lemma:} For all lists $u$ and $v$ we have that
$/rev/[u,v]=/rev/[u,|NIL|]\qapp v$.

\noindent{\bf Proof of Lemma:} The proof of this is by induction on $r↓{list}(u)$ with
$\Phi[u]$ being 
$$\forall v\ /rev/[u,v]=/rev/[u,|NIL|]\qapp v.$$
The base case is overly simple so we only prove the induction step. So 
suppose that $u\in \qL{non-empty}$ and that $\Phi$ holds for lists of less
length (since this is what $r↓{list}$ measures).
Then

$rev[u,v]=\qif \qn u \qthen v \qelse rev[\qd u, \qa u\qcons v]$

and so

$= rev[\qd u, \qa u\qcons v]$

which by the induction hypothesis becomes

$= rev[\qd u, |NIL|]\qapp [\qa u\qcons v]$.

Now by the lemma in the proof of the associativity of /append/ we have
$$\qa u \qcons v  = \qa u \qcons[|NIL|\qapp v] = <\qa u>\qapp v$$
and so we have

$= rev[\qd u, |NIL|]\qapp [<\qa u>\qapp v]$

which by associativity of append and the above exercise showing that
$$rev : \qL!\times\qL!\to\qL!$$

$= rev[\qd u, |NIL|]\qapp  <\qa u>] \qapp v]$

which by the induction hypothesis is just

$= rev[\qd u, <\qa u>]\qapp   v$

and this reduces to

$= rev[\qa u\qcons \qd u, |NIL|]\qapp   v  = rev[u, |NIL|]\qapp   v$

$\qed↓{\bf main\ lemma}$

The proof of the equivalence of /reverse/ and /reverse1/ is now quite simple.

\noindent{\bf Proof of Proposition:}  Is by induction on $r↓{list}(u)$, the base case is
again unproblematic so we content ourselves with the induction step.
Suppose $u\in\qL{non-empty}$ and that
$/reverse/[v] = /reverse1/[v]$ for all lists $v$ of less length.
then

$/reverse/[u]=/rev/[u,|NIL|]$

which is

$=/rev/[\qd u,\qa u \qcons |NIL|]$

$=/rev/[\qd u,<\qa u>]$

which by the main lemma is just

$=/rev/[\qd u, |NIL|]\qapp <\qa u>$

which by definition is

$=/reverse/[\qd u]\qapp <\qa u>$

and using the induction hypothesis we get

$=/reverse1/[\qd u]\qapp <\qa u>$

which by definition is just

$=/reverse1/[u]$

$\qed↓{\bf proposition}$

The next proposition is a fundamental relation between append and reverse.

\noindent{\bf Proposition:}
$\forall u,v\ /reverse/[u\qapp v] =/reverse/[v]\qapp /reverse/[u]$

\noindent{\bf Proof:} Is by induction on the length of $u$, in other words
by induction on $r↓{list}(u)$. $\Phi[u]$ being
$$/reverse/[u\qapp v] =/reverse/[v]\qapp /reverse/[u]$$
As in the previous propositions the base case is very simple so we only
do the induction step. So suppose that $u\in\qL{non-empty}$ and that $\Phi$
holds for all lists of less length. Then

$/reverse/[u\qapp v] =/rev/[u \qapp v, |NIL|]$

which using the definition is

$=/rev/[\qd [u \qapp v], <\qa[u \qapp v]>]$

but $\qa [u \qapp v] = \qa u$ and $\qd [u \qapp v] = \qd u\qapp v$, so

$=/rev/[\qd u \qapp v, <\qa u>]$

which by the main lemma is

$=/rev/[\qd u \qapp v, |NIL|]\qapp <\qa u>$

using the induction hypothesis we get

$=[/reverse/[v]\qapp /reverse/[\qd u]]\qapp <\qa u>$

which by associativity is

$=/reverse/[v]\qapp [/reverse/[\qd u] \qapp <\qa u>]$

using the definition this is

$=/reverse/[v]\qapp [/rev/[\qd u, |NIL|] \qapp <\qa u>]$

which again using the lemma is

$=/reverse/[v]\qapp /rev/[\qd u, <\qa u>]$

and resorting to the definition once more

$=/reverse/[v]\qapp /rev/[\qa u\qcons \qd u, |NIL|]$

$=/reverse/[v]\qapp/reverse/[u]$

$\qed↓{proposition}$

The final property we prove of /reverse/ is that it is its own inverse.

\noindent{\bf Proposition:}
$\forall u\ /reverse/[/reverse/[u]]=u$

\noindent{\bf Proof:} The proof is a simple corollary of the previous proposition.
we again prove it by induction of the length of $u$. Noting that the base case
is immediate. So suppose that $u\in\qL{non-empty}$  and the proposition is true for
all lists of less length.
The crucial observation is that $u = <\qa u>\qapp \qd u$ and so

$/reverse/[/reverse/[u]]=/reverse/[/reverse/[<\qa u>\qapp \qd u]]$

which by the previous proposition is just

$=/reverse/[/reverse/[\qd u]\qapp /reverse/[<\qa u>]]$

which again by the previous proposition is 

$=/reverse/[/reverse/[<\qa u>]]\qapp/reverse/[/reverse/[\qd u]]$

but by the induction hypothesis this is just

$=<\qa u> \qapp \qd u = \qa u \qcons \qd u =u$

$\qed↓{proposition}$